Library midpoint

Require Export PointsETC.
Require Import incidence.

Section Triangle.

Context `{M:triangle_theory}.

Definition midpoint P U :=
 match P,U with
  cTriple p q r, cTriple u v w ⇒
  let h := a×p+b×q+c×r in
  let k := a×u+b×v+c×w in
  cTriple (k×p + h×u) (k×q + h×v) (k×r + h×w)
 end.

Lemma midpoint_col : ∀ A B,
  col A B (midpoint A B).
Proof.
intros.
destruct A;destruct B.
simpl.
unfold col;simpl.
ring.
Qed.

Lemma X5_is_midpoint_of_X3_X4 :
 eq_points X_5 (midpoint X_3 X_4).
Proof.
intros.
red;simpl; repeat split; field; repeat split;try assumption.
Qed.

End Triangle.